Termination Proof Script

Consider the TRS R consisting of the rewrite rules

There are 3 dependency pairs:

The approximated dependency graph contains 2 SCCs: {5} and {7}.

Consider the SCC {5}. There are no usable rules. By taking the AF π with π(L) = π(N) = π(MAX) = 1 together with the lexicographic path order with empty precedence, rule 5 is strictly decreasing.

Consider the SCC {7}. There are no usable rules. By taking the AF π with π(MAX) = 1 and π(N) = [2] together with the lexicographic path order with empty precedence, rule 7 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.02 seconds) --- May 4, 2006